chain-replication-acks{i:l}
chain-replication-acks(es; Cmd; Rsp; isupdate; In; Out; Sys; Ack; f; g; Delta; Q)
== fifo-antecedent(es;Sys;f) & fifo-antecedent(es;Ack;g)
== & (u:E(Sys). (f(u) = u)  ((u  In)))
== & (E(In) r E(Sys))
== & (E(Out) r E(Sys))
== & (E(Out) r E(Ack))
== & (e:E(In). (((isupdate(In(e)))))  ((e  Out)))
== & (e:E(Sys). (((e  In)))  (loc(f(e)) = loc(e))  (((e  Out))))
== & input-forwarding{i:l}
== & input-forwarding(es; Cmd; Sys; isupdate; In; f)
== & (chain:{e:E| ((e  Sys))  ((e  Ack))} (Id List)
== & ((chain-config(es;p-conditional(Ack; Sys);chain)
== & (& chain-consistent(f;chain)
== & (& (e:E(Ack).
== & (& (((loc(g(e)) = loc(e)))
== & (& ( (adjacent(Id;chain(e);loc(e);loc(g(e))) & adjacent(Id;chain(g(e));loc(e);loc(g(e)))))))
== & (e:E(Ack). (loc(g(e)) = loc(e))  ((e  Out)))
== & (e:E(Ack). ((e  Out))  (g(e) = e))
== & (e:E(Ack). (((g(e))  Out))  is-query(In;isupdate;g(e))  (g(e) = e))
== & (e:E(Out).
== & ((is-query(In;isupdate;e)
== & (( (Out(e) = Q(filter(isupdate;es-interface-history(es; Sys; e)),In(e))))
== & (& ((is-query(In;isupdate;e))
== & (& ( (Out(e) = Delta(filter(isupdate;es-interface-history(es; Sys; e))))))
== & (e:E(Ack). Ack(e) = if e  Out then ||filter(isupdate;Sys(e))|| else Ack(g(e)) fi ) 

latex

---

clarification:

chain-replication-acks{i:l}
chain-replication-acks(es; Cmd; Rsp; isupdate; In; Out; Sys; Ack; f; g; Delta; Q)
== fifo-antecedent(es;Sys;f) & fifo-antecedent(es;Ack;g)
== & (u:es-E-interface(es;Sys). (f(u) = u  es-E(es))  ((u  In)))
== & (es-E-interface(es;In) r es-E-interface(es;Sys))
== & (es-E-interface(es;Out) r es-E-interface(es;Sys))
== & (es-E-interface(es;Out) r es-E-interface(es;Ack))
== & (e:es-E-interface(es;In). (((isupdate(In(e)))))  ((e  Out)))
== & (e:es-E-interface(es;Sys).
== & ((((e  In)))  (es-loc(es; (f(e))) = es-loc(es; e)  Id)  (((e  Out))))
== & input-forwarding{i:l}
== & input-forwarding(es; Cmd; Sys; isupdate; In; f)
== & (chain:{e:es-E(es)| ((e  Sys))  ((e  Ack))} (Id List)
== & ((chain-config(es;p-conditional(Ack; Sys);chain)
== & (& chain-consistent(es;Sys;In;isupdate;Out;f;chain)
== & (& (e:es-E-interface(es;Ack).
== & (& (((es-loc(es; (g(e))) = es-loc(es; e)  Id))
== & (& ( (adjacent(Id;chain(e);es-loc(es; e);es-loc(es; (g(e))))
== & (& ( & adjacent(Id;chain(g(e));es-loc(es; e);es-loc(es; (g(e))))))))
== & (e:es-E-interface(es;Ack). (es-loc(es; (g(e))) = es-loc(es; e)  Id)  ((e  Out)))
== & (e:es-E-interface(es;Ack). ((e  Out))  (g(e) = e  es-E(es)))
== & (e:es-E-interface(es;Ack).
== & ((((g(e))  Out))  is-query(In;isupdate;g(e))  (g(e) = e  es-E(es)))
== & (e:es-E-interface(es;Out).
== & ((is-query(In;isupdate;e)
== & (( (Out(e) = Q(filter(isupdate;es-interface-history(es; Sys; e)),In(e))  Rsp))
== & (& ((is-query(In;isupdate;e))
== & (& ( (Out(e) = Delta(filter(isupdate;es-interface-history(es; Sys; e)))  Rsp)))
== & (e:es-E-interface(es;Ack).
== & (Ack(e) = if e  Out then ||filter(isupdate;Sys(e))|| else Ack(g(e)) fi   ) 

latex

Up	abstract chain replication
Wellformedness Lemmas	chain-replication-acks wf
Definitions	fifo-antecedent(es;Sys;f), P  Q, input-forwarding{i:l}(es; Cmd; Sys; isupdate; In; f), x:A. B(x), x:AB(x), {x:A| B(x)} , P  Q, type List, chain-config(es;Sys;chain), p-conditional(f; g), chain-consistent(f;chain), adjacent(T;L;x;y), Id, loc(e), b, E, P & Q, P  Q, A, is-query(In;isupdate;e), es-interface-history(es; X; e), x:A. B(x), E(X), s = t, , if b then t else f fi , e  X, ||as||, filter(P;l), X(e), f(a)
FDL editor aliases	chain-replication-acks